home *** CD-ROM | disk | FTP | other *** search
/ Language/OS - Multiplatform Resource Library / LANGUAGE OS.iso / quintus / quintus0.lha / work / xvisor_2.05.8 < prev   
Text File  |  1992-04-03  |  9KB  |  305 lines
  1. %%% XVISOR
  2. %%% version 2.03.4 (based on xvisor_16.3)
  3. %%%   incorporated changes made to clin V1 between 7/31/90 and 10/18/90 which
  4. %%%     are visible externally -- changes to comments, predicate names, and
  5. %%%     variable names are not incorporated
  6. %%% version 2.05.8
  7. %%%   renamed assign/2 to assign_cmd/2 for compatibility with Quintus Prolog 3
  8. %%%
  9. %%% This is an expert system for the prover HYMAP.
  10. %%% The top level supervisor is intended to help users to run their 
  11. %%% problems without knowing details about the prover.
  12. %%%
  13. %%% The following is the language for users of this expert system:
  14. %%%    problem_list.
  15. %%%    ...
  16. %%%    end.
  17. %%%
  18. %%% The following is the language for experts:
  19. %%%    expert_rule(support_list(S))
  20. %%%    expert_rule(time_limit_coef(F))
  21. %%%     expert_rule(literal_bound(L))
  22. %%%
  23. %%% The algorithm is the following:
  24. %%%    read in problems in an unsolved list UL
  25. %%%    set T = least_time_bound
  26. %%%    make SL empty
  27. %%%    while T =< greatest_time_bound
  28. %%%        while we have next strategy S
  29. %%%            while we have unsolved problem P in UL
  30. %%%                solve P with S within T
  31. %%%                if P is solved
  32. %%%                then delete P from UL and put P in SL
  33. %%%            endwhile
  34. %%%            if UL is empty
  35. %%%            then print out 'all done' and return
  36. %%%        endwhile
  37. %%%        T = 2*T
  38. %%%    endwhile
  39. %%%    print out solved problems in SL and unsolved problems in UL
  40.  
  41. %%% Two modes are provided for top level supervisor:
  42. %%%    batch mode: To use it, set(super_batch) should be executed.
  43. %%%        A file containing a list of problems and commands
  44. %%%        is the only argument of prove(_).
  45. %%%        The list of problems are listed as follows:
  46. %%%        prove(prob1).
  47. %%%        prove(prob2).
  48. %%%        ...
  49. %%%        prove(probn).
  50. %%%    real time mode: the problem to be solved is the only argument of
  51. %%%        prove(_). Users can use assign(least_time_bound,V) and
  52. %%%        assign(greatest_time_bound,V) to set up the time bounds.
  53. %%%    Default is real time mode.
  54. %%%
  55. %%% If a strategy is not complete and it caused a satisfiable result
  56. %%%    for a problem P, then we don't consider this strategy with 
  57. %%%    increased time bound afterwards for P.
  58. %%%
  59. %%% If a problem P failed with errors too_many _input_variables or
  60. %%%    format_error_input_file, then P is removed from the unsolved
  61. %%%    problem list.
  62. %%%
  63. %%% If user doesn't specify necessary clauses for u, o, or n support
  64. %%%    for a problem P, we don't deal with this here.
  65. %%%    The prover would fail at interpretation before trying to prove
  66. %%%    P.
  67. %%%
  68.  
  69. %%% Clear database for supervisor.
  70. %%% Set initial values for supervisor.
  71. %%% Read problem list.
  72. %%% Set initial time limit.
  73. %%% Try to solve all problems.
  74. %%% Reset option values.
  75.      xvisor(File) :-
  76.     not(not(xvisor_clear)),
  77.     not(not(xvisor_set)),
  78.     not(not(xvisor_read_problems(File))),
  79.     not(not(set_initial_time_limit)),
  80.     solve_all_problems,
  81.     reset_options, !.
  82.  
  83. %%% Clear database for supervisor.
  84.      xvisor_clear :-
  85.     abolish(no_try,2),
  86.     abolish(prob_tried_round0,2),
  87.     abolish(solved_prob,1),
  88.     abolish(tried_round0,1),
  89.     abolish(unsolved_prob,1), !.
  90.  
  91. %%% Set options.
  92.      xvisor_set :- 
  93.     set(slidepriority),
  94.     assign_cmd(small_proof_size_bound,100), !.
  95.  
  96. %%% If batch mode, the problem are listed in the given file.
  97.      xvisor_read_problems(File) :-
  98.     super_batch, !,
  99.     read_and_assert_problems_file(File), !.
  100. %%% If not batch mode, the given file is the problem itself.
  101.      xvisor_read_problems(File) :-
  102.     assertz(unsolved_prob(File)),
  103.     assertz(prob_tried_round0(File,0)).
  104.  
  105. %%% Read in problem lists and assert useful information.
  106.      read_and_assert_problems_file(File) :-
  107.     seeing(Input),
  108.     see(File), !,
  109.     interp_problems_file,
  110.     seen,
  111.     see(Input).
  112.  
  113. %%% Interpret the commands in the input file.
  114.      interp_problems_file :-
  115.     read(Term),
  116.          Term \== 'end_of_file', !,
  117.     interp_problems_file(Term), !,
  118.          interp_problems_file.
  119.      interp_problems_file.
  120.  
  121. %%% unsolved problems are stored in two forms:
  122. %%%    unsolved_prob(P)
  123. %%%    prob_tried_round0(P,X)
  124. %%% X is for controlling the execution of round 0.
  125. %%% If a problem P is executed once in a time limit T, then X is set to 1.
  126. %%% So round 0 won't be executed thereafter with other strategies in T.
  127. %%% X should be reset for all unsolved problems if the time limit is 
  128. %%% increased.
  129.      interp_problems_file(prove(P)) :-
  130.     assertz(unsolved_prob(P)), 
  131.     assertz(prob_tried_round0(P,0)), !.
  132.      interp_problems_file(Term) :-
  133.     write_line(5,'ERROR: Wrong input -> ',Term), !, fail.
  134.  
  135. %%% Set initial time limit as least time bound.
  136.      set_initial_time_limit :-
  137.     least_time_bound(T),
  138.     assign_cmd(time_limit,T).
  139.  
  140. %%% Try all problems in one strategy, then next strategy.
  141. %%% If there are unsolved problems when all strategies are tried,
  142. %%% increase the time limit, and try again from the first strategy and
  143. %%% first unsolved problem.
  144. %%% solve_all_problems will stop if either time limit is advanced 
  145. %%% and is greater than greatest time bound, or all problems are solved.
  146.      solve_all_problems :-
  147.     next_strategy(S),
  148.     solve_problems_strategy(S), 
  149.     print_success_message, !.
  150.      solve_all_problems :-
  151.     next_time_limit,
  152.     reset_tried_round0, !,
  153.     solve_all_problems.
  154.      solve_all_problems :-
  155.     write_line(5,'Solved problems:'),
  156.     print_solved_problems,
  157.     write_line(5,'Unsolved problems:'),
  158.     print_unsolved_problems.
  159.  
  160. %%% If solve_problems_strategy succeeds and there are still unsolved 
  161. %%%     problems, then something must be wrong.
  162.      print_success_message :-
  163.     unsolved_prob(_),
  164.     write_line(5,'ERROR: Something must be wrong.'), !.
  165. %%% Otherwise, all problems are solved.
  166.      print_success_message :-
  167.     write_line(5,'All problems solved.').
  168.  
  169. %%% Try with next strategy.
  170.      next_strategy(S) :-
  171.     expert_rule(R),
  172.     what_expert_rule(R,S).
  173.  
  174. %%% Execute rules until support strategy.
  175.      what_expert_rule(support_list(S),S) :-
  176.     assign_cmd(support_list,S), !.
  177.      what_expert_rule(X,_) :-
  178.     X =.. [F,A],
  179.     assign_cmd(F,A), !, fail.
  180.      what_expert_rule(_,_) :-
  181.     fail.
  182.  
  183. %%% Try all unsolved problems one by one with a certain strategy.
  184.      solve_problems_strategy(S) :-
  185.     unsolved_prob(P),
  186.     \+ no_try(P,S),
  187.     hk_tried_round0(P),
  188.     write_line(5,'Try: ',P),
  189.     solve_one_problem(P), !.
  190.      solve_problems_strategy(_) :-
  191.     unsolved_prob(_), !, fail.
  192.      solve_problems_strategy(_).
  193.  
  194. %%% If prove_1 fails, check if there is an error or no user support 
  195. %%%     clauses if user support strategy is specified.
  196.      solve_one_problem(P) :-
  197.     \+ not(not(prove_1(P))),
  198.     !,
  199.     analyze_failure(P).
  200. %%% If prove_1 succeeds, check if the problem was proved or not,
  201. %%%    and update information accordingly.
  202.      solve_one_problem(P) :-
  203.     hk_problem(P), !,
  204.     fail.
  205.  
  206.      analyze_failure(P) :-
  207.     error('too_many_input_variables'),
  208.     remove_problem(P), !, fail.
  209.      analyze_failure(P) :-
  210.     error('Syntactic error in input file !'),
  211.     remove_problem(P), !, fail.
  212.  
  213. %%% Set tried_round0 properly for the next problem to be tried.
  214.      hk_tried_round0(P) :-
  215.     abolish(tried_round0,1),
  216.     prob_tried_round0(P,X),
  217.     assert(tried_round0(X)), !.
  218.  
  219. %%% If the problem is solved, move it to solved_problem list.
  220. %%% Otherwise, update the tried_round0 status for tried problems.
  221.      hk_problem(P) :-
  222.     stop_this_problem(P),
  223.     remove_problem(P), !.
  224.      hk_problem(P) :-
  225.     update_tried_round0(P), !.
  226.     
  227.      remove_problem(P) :-
  228.     retract(unsolved_prob(P)),
  229.     retract(prob_tried_round0(P,_)),
  230.     assertz(solved_prob(P)).
  231.  
  232. %%% If the problem is proved, or if the problem is satisfiable and
  233. %%% the strategy used was a complete strategy.
  234.      stop_this_problem(P) :-
  235.     prove_result(unsatisfiable), !.
  236.      stop_this_problem(P) :-
  237.     support_list(Sup), !,
  238.     prove_result(satisfiable),
  239.     !, process_satisfiable_case(P,Sup).
  240.  
  241. %%% If the strategy is complete, then the problem was solved.
  242. %%% Otherwise, delete all such strategies.
  243.      process_satisfiable_case(_,Sup) :-
  244.     complete_strategy(Sup), !.
  245.      process_satisfiable_case(P,Sup) :-
  246.     assert(no_try(P,Sup)), !, fail.
  247.  
  248. %%% Update tried_round0 information for the problem to avoid executing
  249. %%% round 0 more than once in a certain time limit.
  250.      update_tried_round0(P) :-
  251.     prob_tried_round0(P,1), !.
  252.      update_tried_round0(P) :-
  253.     retract(prob_tried_round0(P,_)),
  254.     assert(prob_tried_round0(P,1)).
  255.  
  256. %%% Update time_limit.
  257. %%% If time_limit is greater than greatest_time_bound, fails.
  258.      next_time_limit :-
  259.     time_limit(T),
  260.     get_time_limit_multiple(F),
  261.     T2 is F*T,
  262.     greatest_time_bound(GT), !,
  263.     T2 =< GT, 
  264.     assign_cmd(time_limit,T2), !.
  265.     
  266.      get_time_limit_multiple(F) :-
  267.     time_limit_multiple(F), !.
  268.      get_time_limit_multiple(2).
  269.     
  270. %%% Reset the tried_round0 status for all unsolved problems,
  271. %%% so that round 0 will be executed for new time_limit.
  272.      reset_tried_round0 :-
  273.     abolish(prob_tried_round0,2),
  274.     reset_tried_round0_1.
  275.  
  276.      reset_tried_round0_1 :-
  277.     unsolved_prob(P),
  278.     assert(prob_tried_round0(P,0)),
  279.     fail.
  280.      reset_tried_round0_1.
  281.  
  282. %%% Print out solved problems.
  283.      print_solved_problems :-
  284.     retract(solved_prob(P)),
  285.     write_line(10,P), 
  286.     fail.
  287.      print_solved_problems.
  288.  
  289. %%% Print out unsolved problems.
  290.      print_unsolved_problems :-
  291.     retract(unsolved_prob(P)),
  292.     retract(prob_tried_round0(P,_)),
  293.     write_line(10,P), 
  294.     fail.
  295.      print_unsolved_problems.
  296.  
  297. %%% Reset options to default values.
  298.      reset_options :-
  299.     clear(slidepriority),
  300.     assign_cmd(small_proof_size_bound,100),
  301.     assign_cmd(support_list,[b,f]),
  302.     assign_cmd(literal_bound,0),
  303.     assign_cmd(time_limit,2000),
  304.     abolish(time_limit_coef,1).
  305.